from z3 import *

s, t, u = Strings("s t u")
prove(
    Implies(
        And(PrefixOf(s, t), SuffixOf(u, t), Length(t) == Length(s) + Length(u)),
        t == Concat(s, u),
    )
)
# > proved

s, t = Consts("s t", SeqSort(IntSort()))
solve(Concat(s, Unit(IntVal(2))) == Concat(Unit(IntVal(1)), t))
prove(Concat(s, Unit(IntVal(2))) != Concat(Unit(IntVal(1)), s))
# > [s = Unit(1), t = Unit(2)]
# > proved